<!DOCTYPE html>
<html>
  <head>
    <meta charset='utf-8'>

    <link rel="stylesheet" type="text/css" 
      href="/assets/css/straybirds.css" media="screen" />
    <link rel="stylesheet" type="text/css" 
      href="/assets/css/pygments.css" media="screen" />

    <!-- MathJax Section Start -->

    <script type="text/javascript"
    src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
    </script>
    <script>
        MathJax.Hub.Config({
              tex2jax: {
              skipTags: ['script', 'noscript', 'style', 'textarea', 'pre']
              }
        });
        MathJax.Hub.Queue(function() {
            var all = MathJax.Hub.getAllJax(), i;
            for(i=0; i < all.length; i += 1) {
                all[i].SourceElement().parentNode.className += ' has-jax';
            }
        });
    </script>

    <!-- MathJax Section End -->

    <!-- Google Analytics Start-->
    <script>
  (function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
  (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
  m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
  })(window,document,'script','//www.google-analytics.com/analytics.js','ga');

  ga('create', 'UA-48100787-1', 'minixalpha.github.io');
  ga('send', 'pageview');

</script>

    <!-- Google Analytics End -->

    <title>Java 内存模型论文阅读</title>
  </head>

  <body>
    <div class="container">
      <header>
        <div class="container">
          <h1>
              <a href="/" title="Home Page"> 潇湘夜雨 </a>
          <span class="github-src">
            <a href ="https://github.com/minixalpha/minixalpha.github.io"
               target="_blank"
               title="Fork me on GitHub">
              <img src="/assets/images/GitHub-Mark-Light-32px.png" alt="">
            </a>
          </span>
          </h1>
        </div>
      </header>

      <aside id="left-side">
        <h2> 分类 </h2>
  <ul class="category-list">
      
            
                <li>
                <a href="/categories/源代码阅读"> 源代码阅读 (20) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/设计模式"> 设计模式 (3) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/科研"> 科研 (6) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/思想"> 思想 (2) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/技术"> 技术 (18) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/工具"> 工具 (4) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/虚拟机"> 虚拟机 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/java"> java (11) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/c语言"> c语言 (4) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/读书"> 读书 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/操作系统"> 操作系统 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/英语"> 英语 (10) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/计算机系统"> 计算机系统 (3) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/生活"> 生活 (1) </a>
                </li>
            
      
  </ul>

      </aside>

      <aside id="right-side">
        <h2> 归档 </h2>
  <ul class="archive-list">
    
    
    
        
        
        
        
            
            <li>
                <a href="/2014/08">
                    2014-08 (1)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/07">
                    2014-07 (5)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/05">
                    2014-05 (12)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/04">
                    2014-04 (3)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/03">
                    2014-03 (11)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/02">
                    2014-02 (6)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/01">
                    2014-01 (3)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2013/11">
                    2013-11 (10)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2013/10">
                    2013-10 (3)
                </a>
            </li>

        
        
    
        
        
        
        
            
            <li>
                <a href="/2010/09">
                    2010-09 (1)
                </a>
            </li>

        
        
    
  </ul>

      </aside>

      <article>

<h1>Java 内存模型论文阅读</h1>

<h2>引言</h2>

<p>Java 的内存模型最早出现在1995年，但是自1997年起，这一内存模型被发现了许多严重的错误和缺陷，它阻碍了很多优化措施，对程序的安全性也没有足够的保证。2001年<a href="https://www.jcp.org/en/jsr/detail?id=133">JSR 133</a>被确立下来，由William Pugh领导，专家组的成员包括了Adve，Doug Lea， William Pugh等。2004年，JSR 133最终版本发布。2005年，Manson  Jeremy, William Pugh, 和 Sarita V. Adve 一同发表了论文 <em>The Java memory model</em>，描述了最新的Java内存模型，这一内存模型在Java 5.0中引入，一直沿用至今。此后，科学家们对Java内存模型进行了进一步的研究的探索，但大的改动并没有出现。</p>

<h2>论文介绍</h2>

<h3>Pugh2000</h3>

<ul>
<li><p>论文名
Pugh W. The Java memory model is fatally flawed[J]. Concurrency - Practice and Experience, 2000, 12(6): 445-455.</p></li>
<li><p>主要内容
介绍了现有Java内存模型的不足之处：
    * 难以理解，不同的人有不同解读
    * 禁止了很多编译器优化，大多数JVM实现都违反Java内存模型
    * 一些常用编程范式违反Java内存模型
    * 没有考虑到在共享内存，弱一致性内存模型下实现Java所带来的一些问题</p></li>
<li><p>参考文献</p>

<ul>
<li>Gontmakher 1997: 证明了Java内存模型需要Coherence</li>
</ul></li>
</ul>

<h3><strong>Manson 2005</strong></h3>

<ul>
<li><p>论文名
Manson J, Pugh W, Adve S V. The Java memory model[M]. ACM, 2005.</p></li>
<li><p>主要内容
JSR 133的成果，介绍了新的Java内存模型，由Java 5.0引入，沿用至今。
基本思想包括：
    * 对满足 Data Race Free 的程序保证顺序一致性(sequential consistency)
    * 对没有正确同步的程序，使用causality的概念加以限制，以保证程序的安全性
    * 新的内存模型足够强，以保证安全性，又足够弱，以保证编译器可以使用足够的优化</p></li>
<li><p>参考文献</p>

<ul>
<li>Lamport 1979: 提出 Sequential Consistency 概念</li>
<li>Relaxed models in academia and commercial hardware
        - Adve 1990
        - Adve 1993
        - Dubois 1986
        - Gharachorloo 1990
        - IBM 1983(System/370 Principles of Operation)
        - May 1994(The PowerPC Architecture)
        - Sites 1995(Alpha AXP Architecture Reference Manual)
        - Weaver 1994(The SPARC Architecture Manual)</li>
<li>SC for DRF
        - Adve 1990
        - Adve 1993
        - Gharachorloo 1990</li>
<li>Flaws in original Java Memory Model
        - Pugh 1999</li>
<li>Original Java Memory Model Research
        - Gosling 1996
        - Kotrajaras 2001
        - Saraswat 2004</li>
</ul></li>
</ul>

<h3><strong>Polyakov 2006</strong></h3>

<ul>
<li><p>论文名
Polyakov S, Schuster A. 
<em>Verification of the Java causality requirements</em>
[M]//Hardware and Software, Verification and Testing. Springer Berlin Heidelberg, 2006: 224-246.</p></li>
<li><p>主要内容
    * 证明验证causality是NP-complete的
    * 跟踪每个线程实际运行时 read 操作的顺序可以简化验证
    * 对可简化的验证提出了多项式算法
    * 不能简化的提出非多项式算法（仅用于短的测试序列）
    * 使用了Post-mortem的方法，实际运行一个多线程程序，在JVM或者定制过的JVM或者模拟器上运行程序，拿到trace，分析trace，以验证内存是否有问题
    * 使用frontier graph验证</p></li>
<li><p>参考文献</p>

<ul>
<li>Boehm 2005: 通过库实现多线程不能保证程序正确性</li>
<li>causal acyclicity 形式化定义(reach condition)：
      -   Suﬃcient System Requirements for  Supporting the PLpc Memory Model. 1993
      -  Specifying System Requirements for Memory Consistency Models. 1993</li>
<li>Gibbons 1993：使用frontier graph验证SC</li>
</ul></li>
</ul>

<h3>Aspinall 2007-1</h3>

<ul>
<li><p>论文名
Aspinall D, Ševčík J. 
<em>Formalising Java’s data race free guarantee</em>
[M]//Theorem Proving in Higher Order Logics. Springer Berlin Heidelberg, 2007: 22-37.</p></li>
<li><p>主要内容</p>

<ul>
<li>给出精确的DRF定义和证明</li>
<li>发现要保证DRF，JMM中并非所有条件都要满足</li>
<li>形式化定义为测试具体实例提供了基础</li>
<li>证明了JMM中给定的条件可以保证DRF</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Huisman 2007</h3>

<ul>
<li><p>论文名
Huisman M, Petri G.
<em>The Java memory model: a formal explanation</em>
[J]. VAMP, 2007, 7: 81-96.</p></li>
<li><p>主要内容</p>

<ul>
<li>使用Coq中形式化描述JMM</li>
<li>证明DRF的条件</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Cenciarelli 2007</h3>

<p><em>论文名
Cenciarelli P, Knapp A, Sibilio E. 
*The Java memory model: Operationally, denotationally, axiomatically</em>
[M]//Programming Languages and Systems. Springer Berlin Heidelberg, 2007: 331-346.</p>

<ul>
<li><p>主要内容</p>

<ul>
<li>构建新的语义框架，由 operational step 构成 denotional model，并被 axioms 限制</li>
<li>使用Configuration Theory 描述 Java 操作规则</li>
<li>为 Java 提供一个基于事件的语义</li>
</ul></li>
</ul>

<h3>Aspinall 2007-2</h3>

<ul>
<li><p>论文名
Aspinall D, Sevcik J.
<em>Java memory model examples: Good, bad and ugly</em>
[J]. VAMP07 Proceedings 2007.</p></li>
<li><p>主要内容</p>

<ul>
<li>Good Example: JMM 允许的行为,展示了非SC的行为和一些优化 </li>
<li>Bad Example:JMM禁止的行为</li>
<li>Ugly Example:JMM禁止,但却出现的行为</li>
<li>通过这些例子展示 Aspinall 2007-1 中提出的形式化定义优于官方定义</li>
</ul></li>
</ul>

<h3>Botinan 2007</h3>

<ul>
<li><p>论文名
Botincan M, Glavan P, Runje D. 
<em>Distributed Algorithms: A Case Study of the Java Memory Model[J].</em>
Proceedings of the ASM, 2007.</p></li>
<li><p>主要内容</p>

<ul>
<li>对 JMM 提供数学化的精确定义</li>
<li>为其在ASM context下提供解释</li>
</ul></li>
</ul>

<h3>Sevcik 2008</h3>

<ul>
<li><p>论文名
Ševčík J, Aspinall D. 
<em>On validity of program transformations in the Java memory model[M]</em>
//ECOOP 2008–Object-Oriented Programming. Springer Berlin Heidelberg, 2008: 27-51.</p></li>
<li><p>主要内容</p>

<ul>
<li>分析了一些常见但在JMM中禁止的优化措施,揭示了  Hotspot JVM 中违背JMM的情况</li>
<li>对data race程序的要求比设计者想的要强</li>
</ul></li>
</ul>

<h3><strong>arnabde 2008</strong></h3>

<ul>
<li><p>论文名
De A, Roychoudhury A, D&#39;Souza D. 
<em>Java memory model aware software validation[C]</em>
//Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering. ACM, 2008: 8-14.</p></li>
<li><p>主要内容</p></li>
</ul>

<p>提出一种近似JMM的内存模型OpMM,它可以与模型检测工具JPF结合,寻找软件中的bug.</p>

<h3><strong>Chen Chen 2009</strong></h3>

<ul>
<li><p>论文名
Chen C, Chen W, Sreedhar V, et al. 
<em>Formalizing Causality as a Desideratum for Memory Models and transformations of Parallel Programs[J].</em>
2009.</p></li>
<li><p>主要内容</p>

<ul>
<li>提出causally ordered,用以构造 causality graph 框架,以找环的方式分析内存模型是否违反 causality</li>
<li>识别出代码转换中保持/违反 causality的措施</li>
<li>提出CMM内存模型,是保证不违反causality的最弱的内存模型</li>
</ul></li>
<li><p>参考文献</p>

<ul>
<li>JMM 社区提出了20 causality test cases,用于编译器和虚拟机验证</li>
</ul></li>
</ul>

<h3>Botincan 2010</h3>

<ul>
<li><p>论文名
Botinčan M, Glavan P, Runje D. Verification of causality requirements in Java memory model is undecidable[M]//Parallel Processing and Applied Mathematics. Springer Berlin Heidelberg, 2010: 62-67.</p></li>
<li><p>主要内容
证明验证任意有限次执行的多线程程序是否满足causality requirments是undecidable的.</p></li>
<li><p>参考文献</p>

<ul>
<li>Polyakov 2006:在无同步操作,final作用域上,通过验证有限次数执行的多线程程序,来验证JMM的causality requirements.证明了在给定的一些假设上,此问题是NP-complete的.</li>
</ul></li>
</ul>

<h3><strong>Torlak 2010</strong></h3>

<ul>
<li><p>论文名
Torlak E, Vaziri M, Dolby J. 
<em>MemSAT: checking axiomatic specifications of memory models[J].</em>
ACM Sigplan Notices, 2010, 45(6): 341-350.</p></li>
<li><p>主要内容</p>

<ul>
<li>基于SAT solver的工具MEMSAT,用于调试推导内存模型,如果给出内存模型的公理化描述,包含断言的多线程程序,工具可以输出一个trace,保证内存模型及多线程程序的断言都得到满足.</li>
<li>在Manson 的 JMM上,以及Sevcik的修复版本上测试过.</li>
<li>第一个对 JMM 的公理化描述进行自动调试推理的工具</li>
</ul></li>
<li><p>参考文献</p>

<ul>
<li>litmus tests 用于对内存模型的形式化说明进行补充,方便人们理解内存模型,验证litmus tests的工作包括:

<ul>
<li>model checking
arnabde 2008: Java memory model aware software validation
yang 2001: Analyzing the CRF Java memory model</li>
<li>constrain solving
Burckhardt 2007: CheckFence: checking consistency of concurrent data types on relaxed memory models
Gopalakrishnan 2004: QB or Not QB: An efﬁcient execution veriﬁcation tool for memory orderings
Yang 2003: Analyzing the Intel Itanium memory ordering rules using logic programming and SAT.</li>
<li>custome search
Sarkar 2009:The semantics of x86–CC multiproces sor machine code
这些工作已经成功对 Intel Itanium x86-CC MM, <strong>JMM</strong> 进行验证,但Aspinall 2007指出了JMM中commiting semantics带来的巨大状态空间使得model checking难以适用.</li>
</ul></li>
<li>Yang 2004:Nemos:a framework for axiomatic and executable speciﬁcations of memory consistency models指出公理语义在描述内存模型上优于操作语义,</li>
<li>Sevcik 2008: 对Manson的JMM进行修复.</li>
<li>JMM 发展历史,相关工作

<ul>
<li>J. Manson JMM simulator</li>
</ul></li>
</ul></li>
</ul>

<h3>Lochbihler 2012</h3>

<ul>
<li><p>论文名
Lochbihler A. 
<em>Java and the Java memory model—A unified, machine-checked formalisation[M]</em>
//Programming Languages and Systems. Springer Berlin Heidelberg, 2012: 497-517.</p></li>
<li><p>主要内容
对 JMM 进行形式化,并通过机器检查,与Java源代码及字节码的操作语义联系在一起.
证明了语义保证了DRF</p></li>
<li><p>参考文献</p>

<ul>
<li>Related Work 介绍的挺全</li>
</ul></li>
</ul>

<h3>Jin 2012</h3>

<ul>
<li><p>论文名
Jin H, Yavuz-Kahveci T, Sanders B A. Java memory model-aware model checking[M]. Springer Berlin Heidelberg, 2012.</p></li>
<li><p>主要内容</p>

<ul>
<li>扩展JPF,产生包含data race的执行</li>
<li>提供工具 Java PathRelaxer(JPR),用于推导包含data race的程序,验证它的性质</li>
</ul></li>
<li><p>参考文献</p>

<ul>
<li>Manson 2002:  The Java memory model simulator</li>
</ul></li>
</ul>

<h3>Demange 2013</h3>

<ul>
<li><p>论文名
Demange D, Laporte V, Zhao L, et al. 
<em>Plan B: A buffered memory model for Java[C]</em>
//ACM SIGPLAN Notices. ACM, 2013, 48(1): 329-342.</p></li>
<li><p>主要内容</p></li>
<li><p>提出了一种新的Java 内存模型BMM,给出公理化定义,刻画了内存事件的次序</p></li>
<li><p>给出BMM&#39;的形式化定义,对Java程序的语义来说,这是一个可操作的定义,容易用于x86体系结构.</p></li>
<li><p>证明BMM和BMM&#39;是一样的</p></li>
<li><p>给出BMM性能测试结果</p></li>
<li><p>相关工作介绍了JMM发展,验证等等.</p></li>
<li><p>参考文献 </p>

<ul>
<li>Sevcik 2011: Relaxed-memory Concurrency and Veriﬁed Compilation</li>
<li>在当前情况下,证明一个编译器是否符合JMM中的定义仍然是一个open的问题.</li>
<li>Sevcik2008: 现存的JVM是不符合JMM的</li>
</ul></li>
</ul>

<h3><strong>LOCHBIHLER 2013</strong></h3>

<ul>
<li><p>论文名
Lochbihler A.
Making the Java memory model safe[J]. 
ACM Transactions on Programming Languages and Systems (TOPLAS), 2013, 35(4): 12.</p></li>
<li><p>主要内容 
    * 基于之前的JinJiaThread语义,为公理语义的JMM提出了一个 <em>unified formalization</em>,将Java与JMM结合在一起
    * 澄清了现有的JMM标准,修复了一些不合适的地方
    * 证明了DRF需要满足的条件</p></li>
<li><p>参考文献</p></li>
</ul>


      </article>

      <div class="comments">
        
          <div id="disqus_thread"></div>
 <script type="text/javascript">
     /* * * CONFIGURATION VARIABLES: EDIT BEFORE PASTING INTO YOUR WEBPAGE * * */
     var disqus_shortname = 'minixalpha'; // required: replace example with your forum shortname

     /* * * DON'T EDIT BELOW THIS LINE * * */
     (function() {
         var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true;
         dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js';
         (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq);
     })();
 </script>
 <noscript>Please enable JavaScript to view the <a href="http://disqus.com/?ref_noscript">comments powered by Disqus.</a></noscript>
    <a href="http://disqus.com" class="dsq-brlink">comments powered by <span class="logo-disqus">Disqus</span></a>
    

        
      </div>


      <footer>
        Copyright (c) minixalpha 2014
      </footer>

    </div>
  </body>
</html>
